l:IdLnk, tg:Id, L:Knd List.
only events in L send on l with tg ||- es.only events in L send on l with tg 

latex

Definitions	es realizer ind Rsframe compseq tag def, Consistent(R;es), ES, t  T, x:A. B(x), only events in L send on lnk with tag, only events in L send on l with tg, x:AB(x), P  Q, True, R-Feasible(R), inr(x), x:AB(x), P & Q, R ||- es.P(es), IdLnk, Id, Knd, type List
Lemmas	Knd wf, Id wf, IdLnk wf, R-consistent wf, Rsframe wf, event system wf